A,B:es_realizer{i:l}. R-discrete_compat(A; B)  R-discrete_compat(B; A) 

latex

Definitions	ff, tt, if b then t else f fi , True, prop{i:l}, t  T, R-discrete_compat(A; B), P  Q, x:A. B(x), P  Q, P  Q, Unit, ,
Lemmas	assert of bnot, eqff to assert, iff transitivity, eqtt to assert, Rinit? wf, Rinit-discrete wf, Rinit-x wf, not wf, bnot wf, assert wf, Reffect-discrete wf, Reffect-x wf, Id wf, bool wf, Reffect? wf, es realizer wf, R-discrete compat wf